Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add cram tests for CFGs #1360

Merged
merged 25 commits into from
Feb 21, 2024
Merged

Add cram tests for CFGs #1360

merged 25 commits into from
Feb 21, 2024

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Feb 9, 2024 •
edited
Loading

This cherry-picks some commits from #847, but uses graph-easy to visualize the .dot output instead of testing the Graphviz code directly.

For end-to-end YAML witness location testing, #1357 is what we finally want, it's not super convenient and general to have to check for node locations through YAML witnesses. This is slightly more direct by both testing the CFG structure (which we've had problems about) and all node locations simultaneously.

TODO

  • Get rid of __goblint_dummy_init, at least in these tests.
  • Go back to per-function CFGs in these tests because 00-sanity/21-empty-loops output is massive only due to the big switch in main, which is orthogonal to the test.
  • Fix GobView (Adapt to compute_cfg move gobview#41).

@sim642 sim642 added the testing label Feb 9, 2024
@sim642 sim642 self-assigned this Feb 9, 2024
@sim642
Move some functions to CfgTools
6ed1aae
@sim642
Test CFGs per function
b727532
@sim642
Fix instructions in CFG testing
a1483d6
@sim642
More detailed location output in CFG tests
361af13
@sim642
Merge branch 'master' into cfg-test
9036370
@sim642
Add test for synthetic witness invariant locations (PR #758)
e81df45
@sim642
Add test for incorrect witness invariant locations from CIL transform…
7018ccf 
…ations (issue #1356)
@sim642
Update CIL for synthetic locations fix
b734f50
@sim642
Add graph-easy Ubuntu depext
65ae0f0
@sim642
Try to pin using with-test in CI
de83ccc
@sim642
Add enabled_if to CFG tests in 00-sanity as well
4d86fd0
@sim642
Try to pin using with-test in CI via opam-depext-flags
d48e85e
@sim642
Try to pin using with-test in CI via hack
4b58d45 
ocaml/opam#3790 (comment).
@sim642
Install graph-easy manually in CI because nothing works
ae5b2cf
@sim642
Install graph-easy only on Ubuntu in CI
15e8ca3
@sim642
Update GobView for moved compute_cfg
d146e9b
@sim642 sim642 mentioned this pull request Feb 14, 2024
Merged
@sim642 sim642 marked this pull request as ready for review February 14, 2024 14:11
michael-schwarz
michael-schwarz reviewed Feb 21, 2024
View reviewed changes
.github/workflows/coverage.yml Outdated Show resolved Hide resolved
tests/regression/cfg/util/cfgDot.ml Outdated Show resolved Hide resolved
src/common/util/cilLocation.ml Outdated Show resolved Hide resolved
@sim642 sim642 added this to the v2.4.0 milestone Feb 21, 2024
@sim642 sim642 merged commit 119592b into master Feb 21, 2024
16 of 17 checks passed
@sim642 sim642 deleted the cfg-test branch February 21, 2024 16:37
@stilscher stilscher mentioned this pull request Feb 26, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@michael-schwarz michael-schwarz michael-schwarz approved these changes

Assignees

@sim642 sim642

Labels
testing
Projects
None yet
Milestone
v2.4.0
Development

Successfully merging this pull request may close these issues.
2 participants
@sim642 @michael-schwarz